$\forall$$T$:Type, $R$:($T$$\rightarrow$$T$$\rightarrow\mathbb{P}$).
\\[0ex]Order($T$;$x$,$y$.$R$($x$,$y$))
\\[0ex]$\Rightarrow$ ($\forall$$x$, $y$:$T$. Dec($x$ = $y$))
\\[0ex]$\Rightarrow$ ($\forall$$a$, $b$:$T$. $R$($a$,$b$) $\Leftarrow\!\Rightarrow$ (strict\_part($x$,$y$.$R$($x$,$y$);$a$;$b$) $\vee$ ($a$ = $b$)))